COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.s(PREFAC, INTRODUCTION)
C00015 ENDMK
C⊗;
.s(PREFAC, INTRODUCTION)
.if NOTASSEMBLING then start
.READIN: NEXT SECTION!;
.WRITIN: NEXT SECTION!;
.PROVIN: NEXT SECTION!;
.PROVEX: NEXT SECTION!;
.IMPURE: NEXT SECTION!;
.MACHIN: NEXT SECTION!;
.SEARCH: NEXT SECTION!;
.EXTEND: NEXT SECTION!;
.ABSNTX: NEXT SECTION!;
.COMPIL: NEXT SECTION!;
.COMPUT: NEXT SECTION!;
.end


	This text is about programming in LISP and proving
facts about LISP programs.

	LISP is a language for programming with symbolic
expressions represented in the computer by list structures.
It is the programming language most used in artificial
intelligence research and is also the most used language
for large systems for computing with mathematical formulas.
Both require extensive computing with symbolic
expressions, and in both it is often just as important to realize
extremely complex algorithms as to make simple algorithms
run as fast as possible.
The data structures and
language of LISP are well suited to this and so is the fact that
LISP programs are represented by LISP data structures; this makes
it easy to write programs that generate new parts of themselves.
This is particularly beneficial in an interactive environment, where
programs that are run only once per human interaction can
transform what is convenient for the user to write into complex
structures of basic operations.

	As a programming language, LISP is characterized by the following
ideas:
.item←0

	#. Computing with symbolic expressions rather than numbers.

	#. Representation of symbolic expressions and other information by
list structure in computer memory.

	#. Representation of information on paper, from keyboards
and in other external media mostly by
multi-level lists and sometimes by S-expressions.  It has been
important that any kind of data can be represented by a single general
type.

	#. A small set of selector and constructor
operations expressed as functions, i.e. ⊗car, ⊗cdr and ⊗cons. 

	#. Composition of functions and conditional expressions
as a major way of building programs from already available functions.

	#. The recursive use of
conditional expressions as a sufficient tool for building computable
functions.

	#. The use of λ-expressions for naming functions.

	#. The storage of information on the property lists of atoms.

	#. Representation of LISP programs as LISP data that can
be manipulated by object programs.  This has prevented the separation
between system programmers and application programmers.  Everyone can
"improve" his LISP, and many of these "improvements" have developed
into improvements to the language.

	#. The LISP function %2eval%1 that
serves both as a formal definition of the language and as an interpreter.

	#. Garbage collection as the means of memory management.

	#. No requirements for declarations so that LISP statements
can be executed in an on-line environment without preliminaries.

	⊗Pure LISP is the core of the language.
Its programs are function expressions which are built up by composition and
conditional expression recursion from basic functions.  These
function expressions are used for their values only and not for side
effects.  This makes them easy to understand and makes LISP recursive
function definitions directly usable as sentences of first order
mathematical logic.  For this reason, proving properties of LISP
functions is very straightforward.

	We believe that a course in programming should include
techniques for proving that the programs meet their specifications.
The programmers should check their correctness proofs by computer
as a replacement for conventional debugging.

	This text goes part of the way to meeting this objective.
It is one of the first to integrate program proving
with programming itself.  Students can be asked to write a program
with given properties and prove that the program has these properties.
The ability to prove the correctness of a program is often a better
criterion for the program being "well structured" than the presence
or absence of specific programming constructs.
Having to prove that a program meets specifications
often induces rewriting it in a more transparent style.

	The major applied objective of research in mathematical
theory of computation should be to make it routine to supply computer
checked proofs of computer program correctness as part of the
process of debugging the program.  To put it strongly, money shouldn't
change hands till this has been done.  Many pure LISP programs have been
proved correct in a course in mathematical theory of computations
using Richard Weyhrauch's FOL proof-checker for first order logic,
though we have not yet used it in the programming course except
as an option in the term project.
The experience of proving facts about programs has the same advantages
as the study of any other mathematical domain.  Even if the student
never proves another theorem, his understanding of the subject is
enhanced by the experience.

	While the mathematical theory of pure LISP is sufficiently
well developed to support computer-checked proofs of correctness,
practical programming also involves constructs whose theories are
still in a primitive state.  These constructs are
described in practical programming terms with some indication
of how their theory is developing.

	The student of LISP should finish the course with four
skills.  First he must understand how to represent symbolic information
in list structures and to read and write LISP programs.  Second
he should understand how to state and prove properties of programs.
Third he should be able to write programs that themselves produce
programs or fragments thereof.  Finally, he should understand the
techniques of one or more major applications of LISP.

	The text begins with a chapter on LISP data structures and
on understanding pure LISP programs.

	Chapter {SECTION WRITIN} tells how
to write pure LISP programs and is organized around the different
kinds of recursion appropriate for different tasks and data
structures.

	Chapter {SECTION PROVIN} shows how to
represent pure LISP programs as sentences of logic and use these
sentences to prove properties of the programs.

	Chapter {SECTION PROVEX} applies the methods of {SECTION provin}
to more difficult problems of proving correctness.

	Chapter {SECTION IMPURE} extends pure LISP with sequential
computations, arrays, macros, property lists, and operations that modify list
structure.

.if false then begin
	Chapter {SECTION extend} discusses proof methods applicable
to sequential programs and methods of proving non-extensional properties
of programs.
.end

	Chapter {SECTION MACHIN} describes how LISP data structures
and programs are represented in a computer and how
LISP interacts with a user at a terminal.

	Chapter {section search} applies LISP to searching graphs
and game trees.

	Chapter {SECTION COMPIL} treats compiling pure LISP programs
as a LISP programming problem.  Two compilers, one short and one
generating fairly efficient code, are given as examples.

	Chapter {SECTION ABSNTX} discusses the notion of abstract
syntax and uses it to prove the correctness of a compiler for a
very simple language fragment.

	Chapter {SECTION COMPUT} discusses some theoretical topics
such as computability and lambda calculus in a framework made easy
by the previous material.

	Not all of the above material can be covered in a one quarter
course.  Additional chapters on pattern directed computing and on
proof methods for impure LISP are will be added.

	The applied material is independent of the theoretical
chapters, but everything depends on the first two chapters.